COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the pigeon hole principle
C00013 00003
C00015 ENDMK
C⊗;
;the pigeon hole principle
(wipe-out)
(get-proofs mult prf ekl sys)

(proof pigeonfacts)

;the arithmetical form of the pigeon hole principle

(axiom |∀f n.(∀m.m≤n⊃natnum f(m))∧(∀m.m<n⊃1≤f(m))∧sum(λk.f(k),n)≤n⊃(∀m.m<n⊃1=f(m))|)
(label pigeonfact)

;the pigeon hole principle on lists

(axiom |∀setseq u.disjoint(setseq,length u)∧
                  (∀k.k<length u⊃1≤mult(u,setseq(k)))⊃
                  (∀k.k<length u⊃1=mult(u,setseq(k)))|)
(label pigeonlist)

(save-proofs pigeon)